#include "buffer_outofbounds.hpp"

buffer_outofbounds::buffer_outofbounds(const CFGvisitorFlatInfo& _flat, const IntervalAnalysis& _iv) 
:	flat(_flat), iv(_iv)
{
}
	
set<label_t> buffer_outofbounds::out_of_bounds() {
	set<label_t> U;	// set of labels in which under or overflow can occur

	for_each(this->flat.labels, [&U, this](CFGvertex* n){
		label_t ell = n->label();
		
		ASTvisitorGetArrays ga;
		set<array_element*> arrays = ga.convert(this->getPayload(n));

		for (auto it = arrays.begin(); it != arrays.end(); ++it) {
			array_element* ae = *it;
			
			IV tmp = this->iv.MFP_entry(ell);
			ASTvisitorAi Ai(tmp);
			Interval ia = Ai.get_interval(ae->index);

			const int max_idx = array_size(ae)-1;
			const bool can_underflow = (ia.lower() < 0);
			const bool can_overflow = (max_idx < ia.upper());
			if (can_underflow) {U.insert(ell);}
			if (can_overflow) {U.insert(ell);}
		}
	});

	return U;
}

int buffer_outofbounds::array_size(array_element *ae) {
	ASTnode *a = ae;

	while (a != NULL) 
	{
		if (TRY_TYPE(program*, prog, a->parent)) 
		{
			assert(prog->sym_tab->declarations[ae->name]->is_array);
			return prog->sym_tab->declarations[ae->name]->array_size;
		}
		a = a->parent;
	}
	return -1;
}

ASTnode* buffer_outofbounds::getPayload(label_t ell0) const {
	return this->getPayload(flat.labels[ell0]);
}

ASTnode* buffer_outofbounds::getPayload(CFGvertex *n) const {
	ASTnode *a = NULL;
	if (TRY_TYPE(box*, b, n)) {
		a = b->payload;
	}
	if (TRY_TYPE(diamond*, d, n)) {
		a = d->condition;
	}
	assert(a);
	return a;
}
